FDL - Step of Proof: nat_ind_tp

Step of Proof: nat_ind_tp

Inference at * 1
Iof proof for Lemma nat ind tp:

1. P :

{k}
2. P(0)
3.

i:

. P(i - 1)

P(i)
4. i :

P(i)

by PushArgs [`hn`,int_to_arg 4]

1:

1:

P(i)

.